| 1. Identity statement | |
| Reference Type | Conference Paper (Conference Proceedings) |
| Site | plutao.sid.inpe.br |
| Holder Code | isadg {BR SPINPE} ibi 8JMKD3MGPCW/3DT298S |
| Identifier | 8JMKD3MGP3W/3GDQ9EB |
| Repository | sid.inpe.br/plutao/2014/06.03.19.45 |
| Last Update | 2014:09.18.13.55.35 (UTC) administrator |
| Metadata Repository | sid.inpe.br/plutao/2014/06.03.19.45.13 |
| Metadata Last Update | 2018:06.04.23.39.30 (UTC) administrator |
| DOI | 10.5220/0004662400050016 |
| ISBN | 9789897580079 |
| Label | lattes: 3237709114127674 1 GerlingerRomeroSchnFerr:2014:UsBaSe |
| Citation Key | RomeroSchnFerr:2014:UsBaSe |
| Title | Using the Base Semantics given by fUML for Verification  |
| Year | 2014 |
| Access Date | 2024, May 18 |
| Secondary Type | PRE CI |
| Number of Files | 1 |
| Size | 838 KiB |
| 2. Context | |
| Author | 1 Romero, Alessandro Gerlinger 2 Schneider, Klaus 3 Ferreira, Maurício Gonçalves Vieira |
| Resume Identifier | 1 2 3 8JMKD3MGP5W/3C9JHT8 |
| Group | 1 CSE-ETES-SPG-INPE-MCTI-GOV-BR 2 3 CRC-CRC-INPE-MCTI-GOV-BR |
| Affiliation | 1 Instituto Nacional de Pesquisas Espaciais (INPE) 2 University of Kaiserslautern 3 Instituto Nacional de Pesquisas Espaciais (INPE) |
| Author e-Mail Address | 1 romgerale@yahoo.com.br 2 schneider@cs.uni-kl.de 3 mauricio@ccs.inpe.br |
| e-Mail Address | marcelo.pazos@inpe.br |
| Conference Name | International Conference on ModelDriven Engineering and Software Development, 2 (MODELSWARD). |
| Conference Location | Lisbon |
| Date | Jan 7-9, 2014 |
| Publisher | SCITEPRESS - Science and and Technology Publications |
| Pages | 5 |
| Book Title | Proceedings |
| Tertiary Type | Paper |
| History (UTC) | 2014-06-03 19:45:13 :: lattes -> administrator :: 2018-06-04 23:39:30 :: administrator -> marcelo.pazos@inpe.br :: 2014 |
| 3. Content and structure | |
| Is the master or a copy? | is the master |
| Content Stage | completed |
| Transferable | 1 |
| Content Type | External Contribution |
| Keywords | Base Semantics fUML UML Alf Formal Methods Theorem Proving Verification |
| Abstract | The lack of formal foundations of UML results in imprecise models since UML only defines graphical notations, but not their formal semantics. However, in safety-critical applications, formal semantics is a requirement for verification. Semantics for the key parts of activities and classes of UML is defined by the semantics of a foundational subset for executable UML models (fUML). Moreover, the base semantics given by fUML defines the formal semantics of UML. In this paper, we evaluate a subset of the base semantics given by fUML covering its formal definition and its use for verification. From the practical perspective, we show with a simple example how the base semantics can support formal verification through theorem proving. The initial results show that the base semantics, when mature, can play an important role in the formal verification of UML models. |
| Area | ETES |
| Arrangement 1 | urlib.net > BDMCI > Fonds > Produção pgr ATUAIS > CSE > Using the Base... |
| Arrangement 2 | urlib.net > BDMCI > Fonds > Produção anterior à 2021 > COCRC > Using the Base... |
| doc Directory Content | access |
| source Directory Content | there are no files |
| agreement Directory Content | there are no files |
| 4. Conditions of access and use | |
| data URL | http://urlib.net/ibi/8JMKD3MGP3W/3GDQ9EB |
| zipped data URL | http://urlib.net/zip/8JMKD3MGP3W/3GDQ9EB |
| Language | en |
| Target File | RoSF14a.pdf |
| User Group | lattes marcelo.pazos@inpe.br |
| Reader Group | administrator marcelo.pazos@inpe.br |
| Visibility | shown |
| Read Permission | allow from all |
| Update Permission | not transferred |
| 5. Allied materials | |
| Mirror Repository | iconet.com.br/banon/2006/11.26.21.31 |
| Next Higher Units | 8JMKD3MGPCW/3F35BSP 8JMKD3MGPCW/3F3PAJE |
| Citing Item List | sid.inpe.br/bibdigital/2013/10.19.00.29 2 sid.inpe.br/bibdigital/2013/10.14.22.20 1 sid.inpe.br/mtc-m21/2012/07.13.14.56.30 1 |
| Host Collection | dpi.inpe.br/plutao@80/2008/08.19.15.01 |
| 6. Notes | |
| Empty Fields | archivingpolicy archivist callnumber copyholder copyright creatorhistory descriptionlevel dissemination edition editor format issn lineage mark nextedition notes numberofvolumes orcid organization parameterlist parentrepositories previousedition previouslowerunit progress project publisheraddress rightsholder schedulinginformation secondarydate secondarykey secondarymark serieseditor session shorttitle sponsor subject tertiarymark type url versiontype volume |
| 7. Description control | |
| e-Mail (login) | marcelo.pazos@inpe.br |
| update | |